es:ES, l:IdLnk, tg:Id, e:E.
isrcv(e)  lnk(e) = l  tag(e) = tg  kind(e) = rcv(l,tg)  Knd 

latex

Definitions	isrcv(e), lnk(e), tag(e), Knd, <a,b>, rcv(l,tg), tag(k), lnk(k), b, isrcv(k), E, ES, Atom$n, Id, x:AB(x), s ~ t, Prop, s = t, IdLnk, SQType(T), {T}, P  Q, kind(e), x:A. B(x), t  T
Lemmas	es-kind wf, isrcv-implies, IdLnk sq, IdLnk wf, Id sq, Id wf, event system wf, es-E wf, isrcv wf, assert wf, lnk wf, tagof wf